r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
↳ QTRS
↳ DependencyPairsProof
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
R(s(x1)) → R(x1)
C(n(x1)) → N(c(x1))
T(n(u(x1))) → R(x1)
R(n(x1)) → R(x1)
R(s(x1)) → S(r(x1))
T(r(u(x1))) → T(c(r(x1)))
R(b(x1)) → S(b(x1))
C(s(x1)) → S(c(x1))
C(r(x1)) → R(c(x1))
C(s(x1)) → C(x1)
S(u(x1)) → S(x1)
R(r(x1)) → S(r(x1))
C(r(x1)) → C(x1)
C(n(x1)) → C(x1)
N(u(x1)) → N(x1)
R(n(x1)) → S(r(x1))
C(u(x1)) → C(x1)
T(r(u(x1))) → C(r(x1))
R(u(x1)) → R(x1)
T(s(u(x1))) → T(c(r(x1)))
T(n(u(x1))) → T(c(r(x1)))
T(s(u(x1))) → C(r(x1))
T(n(u(x1))) → C(r(x1))
T(s(u(x1))) → R(x1)
T(r(u(x1))) → R(x1)
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
R(s(x1)) → R(x1)
C(n(x1)) → N(c(x1))
T(n(u(x1))) → R(x1)
R(n(x1)) → R(x1)
R(s(x1)) → S(r(x1))
T(r(u(x1))) → T(c(r(x1)))
R(b(x1)) → S(b(x1))
C(s(x1)) → S(c(x1))
C(r(x1)) → R(c(x1))
C(s(x1)) → C(x1)
S(u(x1)) → S(x1)
R(r(x1)) → S(r(x1))
C(r(x1)) → C(x1)
C(n(x1)) → C(x1)
N(u(x1)) → N(x1)
R(n(x1)) → S(r(x1))
C(u(x1)) → C(x1)
T(r(u(x1))) → C(r(x1))
R(u(x1)) → R(x1)
T(s(u(x1))) → T(c(r(x1)))
T(n(u(x1))) → T(c(r(x1)))
T(s(u(x1))) → C(r(x1))
T(n(u(x1))) → C(r(x1))
T(s(u(x1))) → R(x1)
T(r(u(x1))) → R(x1)
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
N(u(x1)) → N(x1)
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
N(u(x1)) → N(x1)
The value of delta used in the strict ordering is 4.
POL(N(x1)) = (4)x_1
POL(u(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
S(u(x1)) → S(x1)
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
S(u(x1)) → S(x1)
The value of delta used in the strict ordering is 4.
POL(u(x1)) = 1 + (4)x_1
POL(S(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
R(u(x1)) → R(x1)
R(s(x1)) → R(x1)
R(n(x1)) → R(x1)
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
R(u(x1)) → R(x1)
R(s(x1)) → R(x1)
R(n(x1)) → R(x1)
The value of delta used in the strict ordering is 16.
POL(n(x1)) = 4 + (3)x_1
POL(u(x1)) = 4 + (4)x_1
POL(s(x1)) = 4 + (4)x_1
POL(R(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
C(n(x1)) → C(x1)
C(u(x1)) → C(x1)
C(s(x1)) → C(x1)
C(r(x1)) → C(x1)
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
C(n(x1)) → C(x1)
C(u(x1)) → C(x1)
C(s(x1)) → C(x1)
C(r(x1)) → C(x1)
The value of delta used in the strict ordering is 16.
POL(C(x1)) = (4)x_1
POL(n(x1)) = 4 + (4)x_1
POL(u(x1)) = 4 + x_1
POL(s(x1)) = 4 + (3)x_1
POL(r(x1)) = 4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
T(r(u(x1))) → T(c(r(x1)))
T(s(u(x1))) → T(c(r(x1)))
T(n(u(x1))) → T(c(r(x1)))
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
T(n(u(x1))) → T(c(r(x1)))
Used ordering: Polynomial interpretation [25,35]:
T(r(u(x1))) → T(c(r(x1)))
T(s(u(x1))) → T(c(r(x1)))
The value of delta used in the strict ordering is 8.
POL(T(x1)) = (4)x_1
POL(c(x1)) = x_1
POL(n(x1)) = 4
POL(u(x1)) = 2
POL(r(x1)) = 2
POL(s(x1)) = 2
POL(b(x1)) = 2 + (2)x_1
n(u(x1)) → u(n(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(n(x1)) → n(x1)
r(s(x1)) → s(r(x1))
r(r(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(n(x1)) → s(r(x1))
s(u(x1)) → u(s(x1))
r(u(x1)) → u(r(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
T(r(u(x1))) → T(c(r(x1)))
T(s(u(x1))) → T(c(r(x1)))
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
T(r(u(x1))) → T(c(r(x1)))
Used ordering: Polynomial interpretation [25,35]:
T(s(u(x1))) → T(c(r(x1)))
The value of delta used in the strict ordering is 16.
POL(T(x1)) = (4)x_1
POL(c(x1)) = x_1
POL(n(x1)) = x_1
POL(u(x1)) = 1 + (4)x_1
POL(r(x1)) = 1 + (4)x_1
POL(s(x1)) = x_1
POL(b(x1)) = 0
n(u(x1)) → u(n(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(n(x1)) → n(x1)
r(s(x1)) → s(r(x1))
r(r(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(n(x1)) → s(r(x1))
s(u(x1)) → u(s(x1))
r(u(x1)) → u(r(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
T(s(u(x1))) → T(c(r(x1)))
r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)